IrrelevantMatchRefl.agda:11,9-13
Cannot pattern match against irrelevant argument of type a ≡ b
when checking that the pattern refl has type a ≡ b
